(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun h () Real)
(assert (forall ((g Real)) (xor (<= 0.0 (div (to_int g) (to_int h)) (mod 0 (to_int d)) e) (= c 2.0))))
(assert (= a (div (to_int b) (to_int f))))
(check-sat)
